Inference at * 1 
Iof proof for Lemma fseg transitivity:



1. T : Type
2. l1 : T List
3. l2 : T List
4. l3 : T List
5. L1 : T List
6. l2 = (L1 @ l1)
7. L : T List
8. l3 = (L @ l2)
  L@0:T List. ((L @ L1 @ l1) = (L@0 @ l1)) 

latex

 by ((InstConcl [L @ L1]) 
CollapseTHEN (Auto)) 

latex

C1: 

C1:   (L @ L1 @ l1) = ((L @ L1) @ l1)
C.

Definitions	as @ bs, x:A. B(x), x:A  B(x), Type, type List, , x:A. B(x), x:AB(x), s = t, t  T
Lemmas	append wf